Left Termination of the query pattern
search_tree(g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 183 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 189 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 PiDPToQDPProof (⇒, 0 ms)
        ↳16 QDP
        ↳17 QDPSizeChangeProof (⇔, 0 ms)
        ↳18 YES

(0) Obligation:

Clauses:

search_tree(void).
search_tree(T) :- search_tree(T, X1, X2).
search_tree(tree(X, void, void), X, X).
search_tree(tree(X, void, Right), X, Max) :- ','(search_tree(Right, Min, Max), less(X, Min)).
search_tree(tree(X, Left, void), Min, X) :- ','(search_tree(Left, Min, Max), less(Max, X)).
search_tree(tree(X, Left, Right), Min1, Max2) :- ','(search_tree(Left, Min1, Max1), ','(less(Max1, X), ','(search_tree(Right, Min2, Max2), less(X, Min2)))).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: search_tree(g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

pA(X1, X2, X3, X4) :- search_treeC(X1, X2, X3).
pA(X1, X2, X3, X4) :- ','(search_treecC(X1, X2, X3), lessB(X4, X2)).
search_treeC(tree(X1, void, X2), X1, X3) :- pA(X2, X4, X3, X1).
search_treeC(tree(X1, X2, void), X3, X1) :- pD(X2, X3, X4, X1).
search_treeC(tree(X1, X2, X3), X4, X5) :- pE(X2, X4, X6, X1, X3, X7, X5).
lessB(s(X1), s(X2)) :- lessB(X1, X2).
pD(X1, X2, X3, X4) :- search_treeC(X1, X2, X3).
pD(X1, X2, X3, X4) :- ','(search_treecC(X1, X2, X3), lessB(X3, X4)).
pE(X1, X2, X3, X4, X5, X6, X7) :- search_treeC(X1, X2, X3).
pE(X1, X2, X3, X4, X5, X6, X7) :- ','(search_treecC(X1, X2, X3), lessB(X3, X4)).
pE(X1, X2, X3, X4, X5, X6, X7) :- ','(search_treecC(X1, X2, X3), ','(lesscB(X3, X4), pA(X5, X6, X7, X4))).
search_treeF(tree(X1, void, X2)) :- pA(X2, X3, X4, X1).
search_treeF(tree(X1, X2, void)) :- pD(X2, X3, X4, X1).
search_treeF(tree(X1, X2, X3)) :- pE(X2, X4, X5, X1, X3, X6, X7).

Clauses:

qcA(X1, X2, X3, X4) :- ','(search_treecC(X1, X2, X3), lesscB(X4, X2)).
search_treecC(tree(X1, void, void), X1, X1).
search_treecC(tree(X1, void, X2), X1, X3) :- qcA(X2, X4, X3, X1).
search_treecC(tree(X1, X2, void), X3, X1) :- qcD(X2, X3, X4, X1).
search_treecC(tree(X1, X2, X3), X4, X5) :- qcE(X2, X4, X6, X1, X3, X7, X5).
lesscB(0, s(X1)).
lesscB(s(X1), s(X2)) :- lesscB(X1, X2).
qcD(X1, X2, X3, X4) :- ','(search_treecC(X1, X2, X3), lesscB(X3, X4)).
qcE(X1, X2, X3, X4, X5, X6, X7) :- ','(search_treecC(X1, X2, X3), ','(lesscB(X3, X4), qcA(X5, X6, X7, X4))).

Afs:

search_treeF(x1)  =  search_treeF(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
search_treeF_in: (b)
pA_in: (b,f,f,b)
search_treeC_in: (b,f,f)
search_treecC_in: (b,f,f)
qcA_in: (b,f,f,b)
qcD_in: (b,f,f,b)
qcE_in: (b,f,f,b,b,f,f)
lesscB_in: (b,b)
lessB_in: (b,b)
pD_in: (b,f,f,b)
pE_in: (b,f,f,b,b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

SEARCH_TREEF_IN_G(tree(X1, void, X2)) → U16_G(X1, X2, pA_in_gaag(X2, X3, X4, X1))
SEARCH_TREEF_IN_G(tree(X1, void, X2)) → PA_IN_GAAG(X2, X3, X4, X1)
PA_IN_GAAG(X1, X2, X3, X4) → U1_GAAG(X1, X2, X3, X4, search_treeC_in_gaa(X1, X2, X3))
PA_IN_GAAG(X1, X2, X3, X4) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
SEARCH_TREEC_IN_GAA(tree(X1, void, X2), X1, X3) → U4_GAA(X1, X2, X3, pA_in_gaag(X2, X4, X3, X1))
SEARCH_TREEC_IN_GAA(tree(X1, void, X2), X1, X3) → PA_IN_GAAG(X2, X4, X3, X1)
PA_IN_GAAG(X1, X2, X3, X4) → U2_GAAG(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
U2_GAAG(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U3_GAAG(X1, X2, X3, X4, lessB_in_gg(X4, X2))
U2_GAAG(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → LESSB_IN_GG(X4, X2)
LESSB_IN_GG(s(X1), s(X2)) → U7_GG(X1, X2, lessB_in_gg(X1, X2))
LESSB_IN_GG(s(X1), s(X2)) → LESSB_IN_GG(X1, X2)
SEARCH_TREEC_IN_GAA(tree(X1, X2, void), X3, X1) → U5_GAA(X1, X2, X3, pD_in_gaag(X2, X3, X4, X1))
SEARCH_TREEC_IN_GAA(tree(X1, X2, void), X3, X1) → PD_IN_GAAG(X2, X3, X4, X1)
PD_IN_GAAG(X1, X2, X3, X4) → U8_GAAG(X1, X2, X3, X4, search_treeC_in_gaa(X1, X2, X3))
PD_IN_GAAG(X1, X2, X3, X4) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
SEARCH_TREEC_IN_GAA(tree(X1, X2, X3), X4, X5) → U6_GAA(X1, X2, X3, X4, X5, pE_in_gaaggaa(X2, X4, X6, X1, X3, X7, X5))
SEARCH_TREEC_IN_GAA(tree(X1, X2, X3), X4, X5) → PE_IN_GAAGGAA(X2, X4, X6, X1, X3, X7, X5)
PE_IN_GAAGGAA(X1, X2, X3, X4, X5, X6, X7) → U11_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treeC_in_gaa(X1, X2, X3))
PE_IN_GAAGGAA(X1, X2, X3, X4, X5, X6, X7) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
PE_IN_GAAGGAA(X1, X2, X3, X4, X5, X6, X7) → U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_in_gaa(X1, X2, X3))
U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U13_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lessB_in_gg(X3, X4))
U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → LESSB_IN_GG(X3, X4)
U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U14_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lesscB_in_gg(X3, X4))
U14_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → U15_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, pA_in_gaag(X5, X6, X7, X4))
U14_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → PA_IN_GAAG(X5, X6, X7, X4)
PD_IN_GAAG(X1, X2, X3, X4) → U9_GAAG(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
U9_GAAG(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U10_GAAG(X1, X2, X3, X4, lessB_in_gg(X3, X4))
U9_GAAG(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → LESSB_IN_GG(X3, X4)
SEARCH_TREEF_IN_G(tree(X1, X2, void)) → U17_G(X1, X2, pD_in_gaag(X2, X3, X4, X1))
SEARCH_TREEF_IN_G(tree(X1, X2, void)) → PD_IN_GAAG(X2, X3, X4, X1)
SEARCH_TREEF_IN_G(tree(X1, X2, X3)) → U18_G(X1, X2, X3, pE_in_gaaggaa(X2, X4, X5, X1, X3, X6, X7))
SEARCH_TREEF_IN_G(tree(X1, X2, X3)) → PE_IN_GAAGGAA(X2, X4, X5, X1, X3, X6, X7)

The TRS R consists of the following rules:

search_treecC_in_gaa(tree(X1, void, void), X1, X1) → search_treecC_out_gaa(tree(X1, void, void), X1, X1)
search_treecC_in_gaa(tree(X1, void, X2), X1, X3) → U22_gaa(X1, X2, X3, qcA_in_gaag(X2, X4, X3, X1))
qcA_in_gaag(X1, X2, X3, X4) → U20_gaag(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
search_treecC_in_gaa(tree(X1, X2, void), X3, X1) → U23_gaa(X1, X2, X3, qcD_in_gaag(X2, X3, X4, X1))
qcD_in_gaag(X1, X2, X3, X4) → U26_gaag(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
search_treecC_in_gaa(tree(X1, X2, X3), X4, X5) → U24_gaa(X1, X2, X3, X4, X5, qcE_in_gaaggaa(X2, X4, X6, X1, X3, X7, X5))
qcE_in_gaaggaa(X1, X2, X3, X4, X5, X6, X7) → U28_gaaggaa(X1, X2, X3, X4, X5, X6, X7, search_treecC_in_gaa(X1, X2, X3))
U28_gaaggaa(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U29_gaaggaa(X1, X2, X3, X4, X5, X6, X7, lesscB_in_gg(X3, X4))
lesscB_in_gg(0, s(X1)) → lesscB_out_gg(0, s(X1))
lesscB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lesscB_in_gg(X1, X2))
U25_gg(X1, X2, lesscB_out_gg(X1, X2)) → lesscB_out_gg(s(X1), s(X2))
U29_gaaggaa(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → U30_gaaggaa(X1, X2, X3, X4, X5, X6, X7, qcA_in_gaag(X5, X6, X7, X4))
U30_gaaggaa(X1, X2, X3, X4, X5, X6, X7, qcA_out_gaag(X5, X6, X7, X4)) → qcE_out_gaaggaa(X1, X2, X3, X4, X5, X6, X7)
U24_gaa(X1, X2, X3, X4, X5, qcE_out_gaaggaa(X2, X4, X6, X1, X3, X7, X5)) → search_treecC_out_gaa(tree(X1, X2, X3), X4, X5)
U26_gaag(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U27_gaag(X1, X2, X3, X4, lesscB_in_gg(X3, X4))
U27_gaag(X1, X2, X3, X4, lesscB_out_gg(X3, X4)) → qcD_out_gaag(X1, X2, X3, X4)
U23_gaa(X1, X2, X3, qcD_out_gaag(X2, X3, X4, X1)) → search_treecC_out_gaa(tree(X1, X2, void), X3, X1)
U20_gaag(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U21_gaag(X1, X2, X3, X4, lesscB_in_gg(X4, X2))
U21_gaag(X1, X2, X3, X4, lesscB_out_gg(X4, X2)) → qcA_out_gaag(X1, X2, X3, X4)
U22_gaa(X1, X2, X3, qcA_out_gaag(X2, X4, X3, X1)) → search_treecC_out_gaa(tree(X1, void, X2), X1, X3)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
pA_in_gaag(x1, x2, x3, x4)  =  pA_in_gaag(x1, x4)
search_treeC_in_gaa(x1, x2, x3)  =  search_treeC_in_gaa(x1)
search_treecC_in_gaa(x1, x2, x3)  =  search_treecC_in_gaa(x1)
search_treecC_out_gaa(x1, x2, x3)  =  search_treecC_out_gaa(x1, x2, x3)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x2, x4)
qcA_in_gaag(x1, x2, x3, x4)  =  qcA_in_gaag(x1, x4)
U20_gaag(x1, x2, x3, x4, x5)  =  U20_gaag(x1, x4, x5)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
qcD_in_gaag(x1, x2, x3, x4)  =  qcD_in_gaag(x1, x4)
U26_gaag(x1, x2, x3, x4, x5)  =  U26_gaag(x1, x4, x5)
U24_gaa(x1, x2, x3, x4, x5, x6)  =  U24_gaa(x1, x2, x3, x6)
qcE_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  qcE_in_gaaggaa(x1, x4, x5)
U28_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U28_gaaggaa(x1, x4, x5, x8)
U29_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U29_gaaggaa(x1, x2, x3, x4, x5, x8)
lesscB_in_gg(x1, x2)  =  lesscB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lesscB_out_gg(x1, x2)  =  lesscB_out_gg(x1, x2)
U25_gg(x1, x2, x3)  =  U25_gg(x1, x2, x3)
U30_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U30_gaaggaa(x1, x2, x3, x4, x5, x8)
qcA_out_gaag(x1, x2, x3, x4)  =  qcA_out_gaag(x1, x2, x3, x4)
qcE_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  qcE_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U27_gaag(x1, x2, x3, x4, x5)  =  U27_gaag(x1, x2, x3, x4, x5)
qcD_out_gaag(x1, x2, x3, x4)  =  qcD_out_gaag(x1, x2, x3, x4)
U21_gaag(x1, x2, x3, x4, x5)  =  U21_gaag(x1, x2, x3, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
pD_in_gaag(x1, x2, x3, x4)  =  pD_in_gaag(x1, x4)
pE_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pE_in_gaaggaa(x1, x4, x5)
SEARCH_TREEF_IN_G(x1)  =  SEARCH_TREEF_IN_G(x1)
U16_G(x1, x2, x3)  =  U16_G(x1, x2, x3)
PA_IN_GAAG(x1, x2, x3, x4)  =  PA_IN_GAAG(x1, x4)
U1_GAAG(x1, x2, x3, x4, x5)  =  U1_GAAG(x1, x4, x5)
SEARCH_TREEC_IN_GAA(x1, x2, x3)  =  SEARCH_TREEC_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x2, x4)
U2_GAAG(x1, x2, x3, x4, x5)  =  U2_GAAG(x1, x4, x5)
U3_GAAG(x1, x2, x3, x4, x5)  =  U3_GAAG(x1, x2, x4, x5)
LESSB_IN_GG(x1, x2)  =  LESSB_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x2, x4)
PD_IN_GAAG(x1, x2, x3, x4)  =  PD_IN_GAAG(x1, x4)
U8_GAAG(x1, x2, x3, x4, x5)  =  U8_GAAG(x1, x4, x5)
U6_GAA(x1, x2, x3, x4, x5, x6)  =  U6_GAA(x1, x2, x3, x6)
PE_IN_GAAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PE_IN_GAAGGAA(x1, x4, x5)
U11_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_GAAGGAA(x1, x4, x5, x8)
U12_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAAGGAA(x1, x4, x5, x8)
U13_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GAAGGAA(x1, x2, x4, x5, x8)
U14_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GAAGGAA(x1, x2, x4, x5, x8)
U15_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U15_GAAGGAA(x1, x2, x4, x5, x8)
U9_GAAG(x1, x2, x3, x4, x5)  =  U9_GAAG(x1, x4, x5)
U10_GAAG(x1, x2, x3, x4, x5)  =  U10_GAAG(x1, x2, x4, x5)
U17_G(x1, x2, x3)  =  U17_G(x1, x2, x3)
U18_G(x1, x2, x3, x4)  =  U18_G(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SEARCH_TREEF_IN_G(tree(X1, void, X2)) → U16_G(X1, X2, pA_in_gaag(X2, X3, X4, X1))
SEARCH_TREEF_IN_G(tree(X1, void, X2)) → PA_IN_GAAG(X2, X3, X4, X1)
PA_IN_GAAG(X1, X2, X3, X4) → U1_GAAG(X1, X2, X3, X4, search_treeC_in_gaa(X1, X2, X3))
PA_IN_GAAG(X1, X2, X3, X4) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
SEARCH_TREEC_IN_GAA(tree(X1, void, X2), X1, X3) → U4_GAA(X1, X2, X3, pA_in_gaag(X2, X4, X3, X1))
SEARCH_TREEC_IN_GAA(tree(X1, void, X2), X1, X3) → PA_IN_GAAG(X2, X4, X3, X1)
PA_IN_GAAG(X1, X2, X3, X4) → U2_GAAG(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
U2_GAAG(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U3_GAAG(X1, X2, X3, X4, lessB_in_gg(X4, X2))
U2_GAAG(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → LESSB_IN_GG(X4, X2)
LESSB_IN_GG(s(X1), s(X2)) → U7_GG(X1, X2, lessB_in_gg(X1, X2))
LESSB_IN_GG(s(X1), s(X2)) → LESSB_IN_GG(X1, X2)
SEARCH_TREEC_IN_GAA(tree(X1, X2, void), X3, X1) → U5_GAA(X1, X2, X3, pD_in_gaag(X2, X3, X4, X1))
SEARCH_TREEC_IN_GAA(tree(X1, X2, void), X3, X1) → PD_IN_GAAG(X2, X3, X4, X1)
PD_IN_GAAG(X1, X2, X3, X4) → U8_GAAG(X1, X2, X3, X4, search_treeC_in_gaa(X1, X2, X3))
PD_IN_GAAG(X1, X2, X3, X4) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
SEARCH_TREEC_IN_GAA(tree(X1, X2, X3), X4, X5) → U6_GAA(X1, X2, X3, X4, X5, pE_in_gaaggaa(X2, X4, X6, X1, X3, X7, X5))
SEARCH_TREEC_IN_GAA(tree(X1, X2, X3), X4, X5) → PE_IN_GAAGGAA(X2, X4, X6, X1, X3, X7, X5)
PE_IN_GAAGGAA(X1, X2, X3, X4, X5, X6, X7) → U11_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treeC_in_gaa(X1, X2, X3))
PE_IN_GAAGGAA(X1, X2, X3, X4, X5, X6, X7) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
PE_IN_GAAGGAA(X1, X2, X3, X4, X5, X6, X7) → U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_in_gaa(X1, X2, X3))
U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U13_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lessB_in_gg(X3, X4))
U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → LESSB_IN_GG(X3, X4)
U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U14_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lesscB_in_gg(X3, X4))
U14_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → U15_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, pA_in_gaag(X5, X6, X7, X4))
U14_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → PA_IN_GAAG(X5, X6, X7, X4)
PD_IN_GAAG(X1, X2, X3, X4) → U9_GAAG(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
U9_GAAG(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U10_GAAG(X1, X2, X3, X4, lessB_in_gg(X3, X4))
U9_GAAG(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → LESSB_IN_GG(X3, X4)
SEARCH_TREEF_IN_G(tree(X1, X2, void)) → U17_G(X1, X2, pD_in_gaag(X2, X3, X4, X1))
SEARCH_TREEF_IN_G(tree(X1, X2, void)) → PD_IN_GAAG(X2, X3, X4, X1)
SEARCH_TREEF_IN_G(tree(X1, X2, X3)) → U18_G(X1, X2, X3, pE_in_gaaggaa(X2, X4, X5, X1, X3, X6, X7))
SEARCH_TREEF_IN_G(tree(X1, X2, X3)) → PE_IN_GAAGGAA(X2, X4, X5, X1, X3, X6, X7)

The TRS R consists of the following rules:

search_treecC_in_gaa(tree(X1, void, void), X1, X1) → search_treecC_out_gaa(tree(X1, void, void), X1, X1)
search_treecC_in_gaa(tree(X1, void, X2), X1, X3) → U22_gaa(X1, X2, X3, qcA_in_gaag(X2, X4, X3, X1))
qcA_in_gaag(X1, X2, X3, X4) → U20_gaag(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
search_treecC_in_gaa(tree(X1, X2, void), X3, X1) → U23_gaa(X1, X2, X3, qcD_in_gaag(X2, X3, X4, X1))
qcD_in_gaag(X1, X2, X3, X4) → U26_gaag(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
search_treecC_in_gaa(tree(X1, X2, X3), X4, X5) → U24_gaa(X1, X2, X3, X4, X5, qcE_in_gaaggaa(X2, X4, X6, X1, X3, X7, X5))
qcE_in_gaaggaa(X1, X2, X3, X4, X5, X6, X7) → U28_gaaggaa(X1, X2, X3, X4, X5, X6, X7, search_treecC_in_gaa(X1, X2, X3))
U28_gaaggaa(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U29_gaaggaa(X1, X2, X3, X4, X5, X6, X7, lesscB_in_gg(X3, X4))
lesscB_in_gg(0, s(X1)) → lesscB_out_gg(0, s(X1))
lesscB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lesscB_in_gg(X1, X2))
U25_gg(X1, X2, lesscB_out_gg(X1, X2)) → lesscB_out_gg(s(X1), s(X2))
U29_gaaggaa(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → U30_gaaggaa(X1, X2, X3, X4, X5, X6, X7, qcA_in_gaag(X5, X6, X7, X4))
U30_gaaggaa(X1, X2, X3, X4, X5, X6, X7, qcA_out_gaag(X5, X6, X7, X4)) → qcE_out_gaaggaa(X1, X2, X3, X4, X5, X6, X7)
U24_gaa(X1, X2, X3, X4, X5, qcE_out_gaaggaa(X2, X4, X6, X1, X3, X7, X5)) → search_treecC_out_gaa(tree(X1, X2, X3), X4, X5)
U26_gaag(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U27_gaag(X1, X2, X3, X4, lesscB_in_gg(X3, X4))
U27_gaag(X1, X2, X3, X4, lesscB_out_gg(X3, X4)) → qcD_out_gaag(X1, X2, X3, X4)
U23_gaa(X1, X2, X3, qcD_out_gaag(X2, X3, X4, X1)) → search_treecC_out_gaa(tree(X1, X2, void), X3, X1)
U20_gaag(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U21_gaag(X1, X2, X3, X4, lesscB_in_gg(X4, X2))
U21_gaag(X1, X2, X3, X4, lesscB_out_gg(X4, X2)) → qcA_out_gaag(X1, X2, X3, X4)
U22_gaa(X1, X2, X3, qcA_out_gaag(X2, X4, X3, X1)) → search_treecC_out_gaa(tree(X1, void, X2), X1, X3)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
pA_in_gaag(x1, x2, x3, x4)  =  pA_in_gaag(x1, x4)
search_treeC_in_gaa(x1, x2, x3)  =  search_treeC_in_gaa(x1)
search_treecC_in_gaa(x1, x2, x3)  =  search_treecC_in_gaa(x1)
search_treecC_out_gaa(x1, x2, x3)  =  search_treecC_out_gaa(x1, x2, x3)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x2, x4)
qcA_in_gaag(x1, x2, x3, x4)  =  qcA_in_gaag(x1, x4)
U20_gaag(x1, x2, x3, x4, x5)  =  U20_gaag(x1, x4, x5)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
qcD_in_gaag(x1, x2, x3, x4)  =  qcD_in_gaag(x1, x4)
U26_gaag(x1, x2, x3, x4, x5)  =  U26_gaag(x1, x4, x5)
U24_gaa(x1, x2, x3, x4, x5, x6)  =  U24_gaa(x1, x2, x3, x6)
qcE_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  qcE_in_gaaggaa(x1, x4, x5)
U28_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U28_gaaggaa(x1, x4, x5, x8)
U29_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U29_gaaggaa(x1, x2, x3, x4, x5, x8)
lesscB_in_gg(x1, x2)  =  lesscB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lesscB_out_gg(x1, x2)  =  lesscB_out_gg(x1, x2)
U25_gg(x1, x2, x3)  =  U25_gg(x1, x2, x3)
U30_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U30_gaaggaa(x1, x2, x3, x4, x5, x8)
qcA_out_gaag(x1, x2, x3, x4)  =  qcA_out_gaag(x1, x2, x3, x4)
qcE_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  qcE_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U27_gaag(x1, x2, x3, x4, x5)  =  U27_gaag(x1, x2, x3, x4, x5)
qcD_out_gaag(x1, x2, x3, x4)  =  qcD_out_gaag(x1, x2, x3, x4)
U21_gaag(x1, x2, x3, x4, x5)  =  U21_gaag(x1, x2, x3, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
pD_in_gaag(x1, x2, x3, x4)  =  pD_in_gaag(x1, x4)
pE_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pE_in_gaaggaa(x1, x4, x5)
SEARCH_TREEF_IN_G(x1)  =  SEARCH_TREEF_IN_G(x1)
U16_G(x1, x2, x3)  =  U16_G(x1, x2, x3)
PA_IN_GAAG(x1, x2, x3, x4)  =  PA_IN_GAAG(x1, x4)
U1_GAAG(x1, x2, x3, x4, x5)  =  U1_GAAG(x1, x4, x5)
SEARCH_TREEC_IN_GAA(x1, x2, x3)  =  SEARCH_TREEC_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x2, x4)
U2_GAAG(x1, x2, x3, x4, x5)  =  U2_GAAG(x1, x4, x5)
U3_GAAG(x1, x2, x3, x4, x5)  =  U3_GAAG(x1, x2, x4, x5)
LESSB_IN_GG(x1, x2)  =  LESSB_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x2, x4)
PD_IN_GAAG(x1, x2, x3, x4)  =  PD_IN_GAAG(x1, x4)
U8_GAAG(x1, x2, x3, x4, x5)  =  U8_GAAG(x1, x4, x5)
U6_GAA(x1, x2, x3, x4, x5, x6)  =  U6_GAA(x1, x2, x3, x6)
PE_IN_GAAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PE_IN_GAAGGAA(x1, x4, x5)
U11_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_GAAGGAA(x1, x4, x5, x8)
U12_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAAGGAA(x1, x4, x5, x8)
U13_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GAAGGAA(x1, x2, x4, x5, x8)
U14_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GAAGGAA(x1, x2, x4, x5, x8)
U15_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U15_GAAGGAA(x1, x2, x4, x5, x8)
U9_GAAG(x1, x2, x3, x4, x5)  =  U9_GAAG(x1, x4, x5)
U10_GAAG(x1, x2, x3, x4, x5)  =  U10_GAAG(x1, x2, x4, x5)
U17_G(x1, x2, x3)  =  U17_G(x1, x2, x3)
U18_G(x1, x2, x3, x4)  =  U18_G(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 22 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSB_IN_GG(s(X1), s(X2)) → LESSB_IN_GG(X1, X2)

The TRS R consists of the following rules:

search_treecC_in_gaa(tree(X1, void, void), X1, X1) → search_treecC_out_gaa(tree(X1, void, void), X1, X1)
search_treecC_in_gaa(tree(X1, void, X2), X1, X3) → U22_gaa(X1, X2, X3, qcA_in_gaag(X2, X4, X3, X1))
qcA_in_gaag(X1, X2, X3, X4) → U20_gaag(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
search_treecC_in_gaa(tree(X1, X2, void), X3, X1) → U23_gaa(X1, X2, X3, qcD_in_gaag(X2, X3, X4, X1))
qcD_in_gaag(X1, X2, X3, X4) → U26_gaag(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
search_treecC_in_gaa(tree(X1, X2, X3), X4, X5) → U24_gaa(X1, X2, X3, X4, X5, qcE_in_gaaggaa(X2, X4, X6, X1, X3, X7, X5))
qcE_in_gaaggaa(X1, X2, X3, X4, X5, X6, X7) → U28_gaaggaa(X1, X2, X3, X4, X5, X6, X7, search_treecC_in_gaa(X1, X2, X3))
U28_gaaggaa(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U29_gaaggaa(X1, X2, X3, X4, X5, X6, X7, lesscB_in_gg(X3, X4))
lesscB_in_gg(0, s(X1)) → lesscB_out_gg(0, s(X1))
lesscB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lesscB_in_gg(X1, X2))
U25_gg(X1, X2, lesscB_out_gg(X1, X2)) → lesscB_out_gg(s(X1), s(X2))
U29_gaaggaa(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → U30_gaaggaa(X1, X2, X3, X4, X5, X6, X7, qcA_in_gaag(X5, X6, X7, X4))
U30_gaaggaa(X1, X2, X3, X4, X5, X6, X7, qcA_out_gaag(X5, X6, X7, X4)) → qcE_out_gaaggaa(X1, X2, X3, X4, X5, X6, X7)
U24_gaa(X1, X2, X3, X4, X5, qcE_out_gaaggaa(X2, X4, X6, X1, X3, X7, X5)) → search_treecC_out_gaa(tree(X1, X2, X3), X4, X5)
U26_gaag(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U27_gaag(X1, X2, X3, X4, lesscB_in_gg(X3, X4))
U27_gaag(X1, X2, X3, X4, lesscB_out_gg(X3, X4)) → qcD_out_gaag(X1, X2, X3, X4)
U23_gaa(X1, X2, X3, qcD_out_gaag(X2, X3, X4, X1)) → search_treecC_out_gaa(tree(X1, X2, void), X3, X1)
U20_gaag(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U21_gaag(X1, X2, X3, X4, lesscB_in_gg(X4, X2))
U21_gaag(X1, X2, X3, X4, lesscB_out_gg(X4, X2)) → qcA_out_gaag(X1, X2, X3, X4)
U22_gaa(X1, X2, X3, qcA_out_gaag(X2, X4, X3, X1)) → search_treecC_out_gaa(tree(X1, void, X2), X1, X3)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
search_treecC_in_gaa(x1, x2, x3)  =  search_treecC_in_gaa(x1)
search_treecC_out_gaa(x1, x2, x3)  =  search_treecC_out_gaa(x1, x2, x3)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x2, x4)
qcA_in_gaag(x1, x2, x3, x4)  =  qcA_in_gaag(x1, x4)
U20_gaag(x1, x2, x3, x4, x5)  =  U20_gaag(x1, x4, x5)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
qcD_in_gaag(x1, x2, x3, x4)  =  qcD_in_gaag(x1, x4)
U26_gaag(x1, x2, x3, x4, x5)  =  U26_gaag(x1, x4, x5)
U24_gaa(x1, x2, x3, x4, x5, x6)  =  U24_gaa(x1, x2, x3, x6)
qcE_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  qcE_in_gaaggaa(x1, x4, x5)
U28_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U28_gaaggaa(x1, x4, x5, x8)
U29_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U29_gaaggaa(x1, x2, x3, x4, x5, x8)
lesscB_in_gg(x1, x2)  =  lesscB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lesscB_out_gg(x1, x2)  =  lesscB_out_gg(x1, x2)
U25_gg(x1, x2, x3)  =  U25_gg(x1, x2, x3)
U30_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U30_gaaggaa(x1, x2, x3, x4, x5, x8)
qcA_out_gaag(x1, x2, x3, x4)  =  qcA_out_gaag(x1, x2, x3, x4)
qcE_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  qcE_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U27_gaag(x1, x2, x3, x4, x5)  =  U27_gaag(x1, x2, x3, x4, x5)
qcD_out_gaag(x1, x2, x3, x4)  =  qcD_out_gaag(x1, x2, x3, x4)
U21_gaag(x1, x2, x3, x4, x5)  =  U21_gaag(x1, x2, x3, x4, x5)
LESSB_IN_GG(x1, x2)  =  LESSB_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSB_IN_GG(s(X1), s(X2)) → LESSB_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSB_IN_GG(s(X1), s(X2)) → LESSB_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSB_IN_GG(s(X1), s(X2)) → LESSB_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PA_IN_GAAG(X1, X2, X3, X4) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
SEARCH_TREEC_IN_GAA(tree(X1, void, X2), X1, X3) → PA_IN_GAAG(X2, X4, X3, X1)
SEARCH_TREEC_IN_GAA(tree(X1, X2, void), X3, X1) → PD_IN_GAAG(X2, X3, X4, X1)
PD_IN_GAAG(X1, X2, X3, X4) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
SEARCH_TREEC_IN_GAA(tree(X1, X2, X3), X4, X5) → PE_IN_GAAGGAA(X2, X4, X6, X1, X3, X7, X5)
PE_IN_GAAGGAA(X1, X2, X3, X4, X5, X6, X7) → SEARCH_TREEC_IN_GAA(X1, X2, X3)
PE_IN_GAAGGAA(X1, X2, X3, X4, X5, X6, X7) → U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_in_gaa(X1, X2, X3))
U12_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U14_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lesscB_in_gg(X3, X4))
U14_GAAGGAA(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → PA_IN_GAAG(X5, X6, X7, X4)

The TRS R consists of the following rules:

search_treecC_in_gaa(tree(X1, void, void), X1, X1) → search_treecC_out_gaa(tree(X1, void, void), X1, X1)
search_treecC_in_gaa(tree(X1, void, X2), X1, X3) → U22_gaa(X1, X2, X3, qcA_in_gaag(X2, X4, X3, X1))
qcA_in_gaag(X1, X2, X3, X4) → U20_gaag(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
search_treecC_in_gaa(tree(X1, X2, void), X3, X1) → U23_gaa(X1, X2, X3, qcD_in_gaag(X2, X3, X4, X1))
qcD_in_gaag(X1, X2, X3, X4) → U26_gaag(X1, X2, X3, X4, search_treecC_in_gaa(X1, X2, X3))
search_treecC_in_gaa(tree(X1, X2, X3), X4, X5) → U24_gaa(X1, X2, X3, X4, X5, qcE_in_gaaggaa(X2, X4, X6, X1, X3, X7, X5))
qcE_in_gaaggaa(X1, X2, X3, X4, X5, X6, X7) → U28_gaaggaa(X1, X2, X3, X4, X5, X6, X7, search_treecC_in_gaa(X1, X2, X3))
U28_gaaggaa(X1, X2, X3, X4, X5, X6, X7, search_treecC_out_gaa(X1, X2, X3)) → U29_gaaggaa(X1, X2, X3, X4, X5, X6, X7, lesscB_in_gg(X3, X4))
lesscB_in_gg(0, s(X1)) → lesscB_out_gg(0, s(X1))
lesscB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lesscB_in_gg(X1, X2))
U25_gg(X1, X2, lesscB_out_gg(X1, X2)) → lesscB_out_gg(s(X1), s(X2))
U29_gaaggaa(X1, X2, X3, X4, X5, X6, X7, lesscB_out_gg(X3, X4)) → U30_gaaggaa(X1, X2, X3, X4, X5, X6, X7, qcA_in_gaag(X5, X6, X7, X4))
U30_gaaggaa(X1, X2, X3, X4, X5, X6, X7, qcA_out_gaag(X5, X6, X7, X4)) → qcE_out_gaaggaa(X1, X2, X3, X4, X5, X6, X7)
U24_gaa(X1, X2, X3, X4, X5, qcE_out_gaaggaa(X2, X4, X6, X1, X3, X7, X5)) → search_treecC_out_gaa(tree(X1, X2, X3), X4, X5)
U26_gaag(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U27_gaag(X1, X2, X3, X4, lesscB_in_gg(X3, X4))
U27_gaag(X1, X2, X3, X4, lesscB_out_gg(X3, X4)) → qcD_out_gaag(X1, X2, X3, X4)
U23_gaa(X1, X2, X3, qcD_out_gaag(X2, X3, X4, X1)) → search_treecC_out_gaa(tree(X1, X2, void), X3, X1)
U20_gaag(X1, X2, X3, X4, search_treecC_out_gaa(X1, X2, X3)) → U21_gaag(X1, X2, X3, X4, lesscB_in_gg(X4, X2))
U21_gaag(X1, X2, X3, X4, lesscB_out_gg(X4, X2)) → qcA_out_gaag(X1, X2, X3, X4)
U22_gaa(X1, X2, X3, qcA_out_gaag(X2, X4, X3, X1)) → search_treecC_out_gaa(tree(X1, void, X2), X1, X3)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
search_treecC_in_gaa(x1, x2, x3)  =  search_treecC_in_gaa(x1)
search_treecC_out_gaa(x1, x2, x3)  =  search_treecC_out_gaa(x1, x2, x3)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x2, x4)
qcA_in_gaag(x1, x2, x3, x4)  =  qcA_in_gaag(x1, x4)
U20_gaag(x1, x2, x3, x4, x5)  =  U20_gaag(x1, x4, x5)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
qcD_in_gaag(x1, x2, x3, x4)  =  qcD_in_gaag(x1, x4)
U26_gaag(x1, x2, x3, x4, x5)  =  U26_gaag(x1, x4, x5)
U24_gaa(x1, x2, x3, x4, x5, x6)  =  U24_gaa(x1, x2, x3, x6)
qcE_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  qcE_in_gaaggaa(x1, x4, x5)
U28_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U28_gaaggaa(x1, x4, x5, x8)
U29_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U29_gaaggaa(x1, x2, x3, x4, x5, x8)
lesscB_in_gg(x1, x2)  =  lesscB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lesscB_out_gg(x1, x2)  =  lesscB_out_gg(x1, x2)
U25_gg(x1, x2, x3)  =  U25_gg(x1, x2, x3)
U30_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U30_gaaggaa(x1, x2, x3, x4, x5, x8)
qcA_out_gaag(x1, x2, x3, x4)  =  qcA_out_gaag(x1, x2, x3, x4)
qcE_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  qcE_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U27_gaag(x1, x2, x3, x4, x5)  =  U27_gaag(x1, x2, x3, x4, x5)
qcD_out_gaag(x1, x2, x3, x4)  =  qcD_out_gaag(x1, x2, x3, x4)
U21_gaag(x1, x2, x3, x4, x5)  =  U21_gaag(x1, x2, x3, x4, x5)
PA_IN_GAAG(x1, x2, x3, x4)  =  PA_IN_GAAG(x1, x4)
SEARCH_TREEC_IN_GAA(x1, x2, x3)  =  SEARCH_TREEC_IN_GAA(x1)
PD_IN_GAAG(x1, x2, x3, x4)  =  PD_IN_GAAG(x1, x4)
PE_IN_GAAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PE_IN_GAAGGAA(x1, x4, x5)
U12_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAAGGAA(x1, x4, x5, x8)
U14_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GAAGGAA(x1, x2, x4, x5, x8)

We have to consider all (P,R,Pi)-chains

(15) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PA_IN_GAAG(X1, X4) → SEARCH_TREEC_IN_GAA(X1)
SEARCH_TREEC_IN_GAA(tree(X1, void, X2)) → PA_IN_GAAG(X2, X1)
SEARCH_TREEC_IN_GAA(tree(X1, X2, void)) → PD_IN_GAAG(X2, X1)
PD_IN_GAAG(X1, X4) → SEARCH_TREEC_IN_GAA(X1)
SEARCH_TREEC_IN_GAA(tree(X1, X2, X3)) → PE_IN_GAAGGAA(X2, X1, X3)
PE_IN_GAAGGAA(X1, X4, X5) → SEARCH_TREEC_IN_GAA(X1)
PE_IN_GAAGGAA(X1, X4, X5) → U12_GAAGGAA(X1, X4, X5, search_treecC_in_gaa(X1))
U12_GAAGGAA(X1, X4, X5, search_treecC_out_gaa(X1, X2, X3)) → U14_GAAGGAA(X1, X2, X4, X5, lesscB_in_gg(X3, X4))
U14_GAAGGAA(X1, X2, X4, X5, lesscB_out_gg(X3, X4)) → PA_IN_GAAG(X5, X4)

The TRS R consists of the following rules:

search_treecC_in_gaa(tree(X1, void, void)) → search_treecC_out_gaa(tree(X1, void, void), X1, X1)
search_treecC_in_gaa(tree(X1, void, X2)) → U22_gaa(X1, X2, qcA_in_gaag(X2, X1))
qcA_in_gaag(X1, X4) → U20_gaag(X1, X4, search_treecC_in_gaa(X1))
search_treecC_in_gaa(tree(X1, X2, void)) → U23_gaa(X1, X2, qcD_in_gaag(X2, X1))
qcD_in_gaag(X1, X4) → U26_gaag(X1, X4, search_treecC_in_gaa(X1))
search_treecC_in_gaa(tree(X1, X2, X3)) → U24_gaa(X1, X2, X3, qcE_in_gaaggaa(X2, X1, X3))
qcE_in_gaaggaa(X1, X4, X5) → U28_gaaggaa(X1, X4, X5, search_treecC_in_gaa(X1))
U28_gaaggaa(X1, X4, X5, search_treecC_out_gaa(X1, X2, X3)) → U29_gaaggaa(X1, X2, X3, X4, X5, lesscB_in_gg(X3, X4))
lesscB_in_gg(0, s(X1)) → lesscB_out_gg(0, s(X1))
lesscB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lesscB_in_gg(X1, X2))
U25_gg(X1, X2, lesscB_out_gg(X1, X2)) → lesscB_out_gg(s(X1), s(X2))
U29_gaaggaa(X1, X2, X3, X4, X5, lesscB_out_gg(X3, X4)) → U30_gaaggaa(X1, X2, X3, X4, X5, qcA_in_gaag(X5, X4))
U30_gaaggaa(X1, X2, X3, X4, X5, qcA_out_gaag(X5, X6, X7, X4)) → qcE_out_gaaggaa(X1, X2, X3, X4, X5, X6, X7)
U24_gaa(X1, X2, X3, qcE_out_gaaggaa(X2, X4, X6, X1, X3, X7, X5)) → search_treecC_out_gaa(tree(X1, X2, X3), X4, X5)
U26_gaag(X1, X4, search_treecC_out_gaa(X1, X2, X3)) → U27_gaag(X1, X2, X3, X4, lesscB_in_gg(X3, X4))
U27_gaag(X1, X2, X3, X4, lesscB_out_gg(X3, X4)) → qcD_out_gaag(X1, X2, X3, X4)
U23_gaa(X1, X2, qcD_out_gaag(X2, X3, X4, X1)) → search_treecC_out_gaa(tree(X1, X2, void), X3, X1)
U20_gaag(X1, X4, search_treecC_out_gaa(X1, X2, X3)) → U21_gaag(X1, X2, X3, X4, lesscB_in_gg(X4, X2))
U21_gaag(X1, X2, X3, X4, lesscB_out_gg(X4, X2)) → qcA_out_gaag(X1, X2, X3, X4)
U22_gaa(X1, X2, qcA_out_gaag(X2, X4, X3, X1)) → search_treecC_out_gaa(tree(X1, void, X2), X1, X3)

The set Q consists of the following terms:

search_treecC_in_gaa(x0)
qcA_in_gaag(x0, x1)
qcD_in_gaag(x0, x1)
qcE_in_gaaggaa(x0, x1, x2)
U28_gaaggaa(x0, x1, x2, x3)
lesscB_in_gg(x0, x1)
U25_gg(x0, x1, x2)
U29_gaaggaa(x0, x1, x2, x3, x4, x5)
U30_gaaggaa(x0, x1, x2, x3, x4, x5)
U24_gaa(x0, x1, x2, x3)
U26_gaag(x0, x1, x2)
U27_gaag(x0, x1, x2, x3, x4)
U23_gaa(x0, x1, x2)
U20_gaag(x0, x1, x2)
U21_gaag(x0, x1, x2, x3, x4)
U22_gaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(17) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SEARCH_TREEC_IN_GAA(tree(X1, void, X2)) → PA_IN_GAAG(X2, X1)
    The graph contains the following edges 1 > 1, 1 > 2

  • U14_GAAGGAA(X1, X2, X4, X5, lesscB_out_gg(X3, X4)) → PA_IN_GAAG(X5, X4)
    The graph contains the following edges 4 >= 1, 3 >= 2, 5 > 2

  • PA_IN_GAAG(X1, X4) → SEARCH_TREEC_IN_GAA(X1)
    The graph contains the following edges 1 >= 1

  • PD_IN_GAAG(X1, X4) → SEARCH_TREEC_IN_GAA(X1)
    The graph contains the following edges 1 >= 1

  • PE_IN_GAAGGAA(X1, X4, X5) → SEARCH_TREEC_IN_GAA(X1)
    The graph contains the following edges 1 >= 1

  • SEARCH_TREEC_IN_GAA(tree(X1, X2, void)) → PD_IN_GAAG(X2, X1)
    The graph contains the following edges 1 > 1, 1 > 2

  • SEARCH_TREEC_IN_GAA(tree(X1, X2, X3)) → PE_IN_GAAGGAA(X2, X1, X3)
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

  • PE_IN_GAAGGAA(X1, X4, X5) → U12_GAAGGAA(X1, X4, X5, search_treecC_in_gaa(X1))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U12_GAAGGAA(X1, X4, X5, search_treecC_out_gaa(X1, X2, X3)) → U14_GAAGGAA(X1, X2, X4, X5, lesscB_in_gg(X3, X4))
    The graph contains the following edges 1 >= 1, 4 > 1, 4 > 2, 2 >= 3, 3 >= 4

(18) YES